0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 88 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 21 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 MRRProof (⇔, 28 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
permB_in_ga([], []) → permB_out_ga([], [])
permB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permB_in_ga(T22, T23))
permB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permB_out_ga(.(T37, T38), .(T39, T40))
permB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permB_out_ga(.(T37, T45), T46)) → permB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permB_out_ga(T22, T23)) → permB_out_ga(.(T21, T22), .(T21, T23))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
permB_in_ga([], []) → permB_out_ga([], [])
permB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permB_in_ga(T22, T23))
permB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permB_out_ga(.(T37, T38), .(T39, T40))
permB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permB_out_ga(.(T37, T45), T46)) → permB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permB_out_ga(T22, T23)) → permB_out_ga(.(T21, T22), .(T21, T23))
PERMB_IN_GA(.(T21, T22), .(T21, T23)) → U2_GA(T21, T22, T23, permB_in_ga(T22, T23))
PERMB_IN_GA(.(T21, T22), .(T21, T23)) → PERMB_IN_GA(T22, T23)
PERMB_IN_GA(.(T37, T38), .(T39, T40)) → U3_GA(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
PERMB_IN_GA(.(T37, T38), .(T39, T40)) → DELETEA_IN_AGA(T39, T38, X42)
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → U1_AGA(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → DELETEA_IN_AGA(T70, T69, X75)
PERMB_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_GA(T37, T38, T39, T46, permB_in_ga(.(T37, T45), T46))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → PERMB_IN_GA(.(T37, T45), T46)
permB_in_ga([], []) → permB_out_ga([], [])
permB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permB_in_ga(T22, T23))
permB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permB_out_ga(.(T37, T38), .(T39, T40))
permB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permB_out_ga(.(T37, T45), T46)) → permB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permB_out_ga(T22, T23)) → permB_out_ga(.(T21, T22), .(T21, T23))
PERMB_IN_GA(.(T21, T22), .(T21, T23)) → U2_GA(T21, T22, T23, permB_in_ga(T22, T23))
PERMB_IN_GA(.(T21, T22), .(T21, T23)) → PERMB_IN_GA(T22, T23)
PERMB_IN_GA(.(T37, T38), .(T39, T40)) → U3_GA(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
PERMB_IN_GA(.(T37, T38), .(T39, T40)) → DELETEA_IN_AGA(T39, T38, X42)
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → U1_AGA(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → DELETEA_IN_AGA(T70, T69, X75)
PERMB_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_GA(T37, T38, T39, T46, permB_in_ga(.(T37, T45), T46))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → PERMB_IN_GA(.(T37, T45), T46)
permB_in_ga([], []) → permB_out_ga([], [])
permB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permB_in_ga(T22, T23))
permB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permB_out_ga(.(T37, T38), .(T39, T40))
permB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permB_out_ga(.(T37, T45), T46)) → permB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permB_out_ga(T22, T23)) → permB_out_ga(.(T21, T22), .(T21, T23))
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → DELETEA_IN_AGA(T70, T69, X75)
permB_in_ga([], []) → permB_out_ga([], [])
permB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permB_in_ga(T22, T23))
permB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permB_out_ga(.(T37, T38), .(T39, T40))
permB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permB_out_ga(.(T37, T45), T46)) → permB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permB_out_ga(T22, T23)) → permB_out_ga(.(T21, T22), .(T21, T23))
DELETEA_IN_AGA(T70, .(T68, T69), .(T68, X75)) → DELETEA_IN_AGA(T70, T69, X75)
DELETEA_IN_AGA(.(T68, T69)) → DELETEA_IN_AGA(T69)
From the DPs we obtained the following set of size-change graphs:
PERMB_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → PERMB_IN_GA(.(T37, T45), T46)
PERMB_IN_GA(.(T21, T22), .(T21, T23)) → PERMB_IN_GA(T22, T23)
permB_in_ga([], []) → permB_out_ga([], [])
permB_in_ga(.(T21, T22), .(T21, T23)) → U2_ga(T21, T22, T23, permB_in_ga(T22, T23))
permB_in_ga(.(T37, T38), .(T39, T40)) → U3_ga(T37, T38, T39, T40, deleteA_in_aga(T39, T38, X42))
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
U3_ga(T37, T38, T39, T40, deleteA_out_aga(T39, T38, X42)) → permB_out_ga(.(T37, T38), .(T39, T40))
permB_in_ga(.(T37, T38), .(T39, T46)) → U4_ga(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_ga(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → U5_ga(T37, T38, T39, T46, permB_in_ga(.(T37, T45), T46))
U5_ga(T37, T38, T39, T46, permB_out_ga(.(T37, T45), T46)) → permB_out_ga(.(T37, T38), .(T39, T46))
U2_ga(T21, T22, T23, permB_out_ga(T22, T23)) → permB_out_ga(.(T21, T22), .(T21, T23))
PERMB_IN_GA(.(T37, T38), .(T39, T46)) → U4_GA(T37, T38, T39, T46, deleteA_in_aga(T39, T38, T45))
U4_GA(T37, T38, T39, T46, deleteA_out_aga(T39, T38, T45)) → PERMB_IN_GA(.(T37, T45), T46)
PERMB_IN_GA(.(T21, T22), .(T21, T23)) → PERMB_IN_GA(T22, T23)
deleteA_in_aga(T59, .(T59, T60), T60) → deleteA_out_aga(T59, .(T59, T60), T60)
deleteA_in_aga(T70, .(T68, T69), .(T68, X75)) → U1_aga(T70, T68, T69, X75, deleteA_in_aga(T70, T69, X75))
U1_aga(T70, T68, T69, X75, deleteA_out_aga(T70, T69, X75)) → deleteA_out_aga(T70, .(T68, T69), .(T68, X75))
PERMB_IN_GA(.(T37, T38)) → U4_GA(T37, deleteA_in_aga(T38))
U4_GA(T37, deleteA_out_aga(T39, T45)) → PERMB_IN_GA(.(T37, T45))
PERMB_IN_GA(.(T21, T22)) → PERMB_IN_GA(T22)
deleteA_in_aga(.(T59, T60)) → deleteA_out_aga(T59, T60)
deleteA_in_aga(.(T68, T69)) → U1_aga(T68, deleteA_in_aga(T69))
U1_aga(T68, deleteA_out_aga(T70, X75)) → deleteA_out_aga(T70, .(T68, X75))
deleteA_in_aga(x0)
U1_aga(x0, x1)
PERMB_IN_GA(.(T37, T38)) → U4_GA(T37, deleteA_in_aga(T38))
U4_GA(T37, deleteA_out_aga(T39, T45)) → PERMB_IN_GA(.(T37, T45))
PERMB_IN_GA(.(T21, T22)) → PERMB_IN_GA(T22)
deleteA_in_aga(.(T59, T60)) → deleteA_out_aga(T59, T60)
deleteA_in_aga(.(T68, T69)) → U1_aga(T68, deleteA_in_aga(T69))
U1_aga(T68, deleteA_out_aga(T70, X75)) → deleteA_out_aga(T70, .(T68, X75))
PERMBINGA1 > U4GA2 > deleteAinaga1 > U1aga2 > deleteAoutaga2 > .2
deleteA_in_aga_1=1
PERMB_IN_GA_1=1
._2=1
deleteA_out_aga_2=2
U1_aga_2=1
U4_GA_2=0
deleteA_in_aga(x0)
U1_aga(x0, x1)